nLab adjunction

Redirected from "adjoint pairs".
Contents

This page is about adjunctions in general 2-categories. Specifically for the common case of adjunctions in Cat see at adjoint functors. For the notion of “adjunction of a set to a field” in field theory, see field extension.

Contents

Idea

A pair of 1-morphisms in a 2-category form an adjunction if they are dual to each other (Lambek (1982), cf. here) in a precise sense.

There are two archetypical classes of examples:

Finally, the notion of adjunction may usefully be thought of as a generalization of the notion of equivalence in a 2-category: an adjoint 1-morphism need not be invertible (even up to 2-isomorphism) but it does have, in a precise sense, a left inverse from below or a right inverse from above.

If an adjoint 1-morphisms happens to be a genuine equivalence in a 2-category, then the adjunction is called an adjoint equivalence.

Definition

Definition

An adjunction in a 2-category is

such that the following equivalent conditions hold:

In terms of string diagrams the above data entering the definition looks like

String diagram for a left adjoint (for 'Adjunction')         String diagram of a right adjoint (for 'Adjunction')          String diagram of an adjunction unit (for 'Adjunction')          String diagram of an adjunction co-unit (for 'Adjunction')

(where 1-cells read from right to left and 2-cells from bottom to top), and the zig-zag identities appear as moves “pulling zigzags straight” (hence the name):

String diagram of first zigzag identity (for 'Adjunction')        

Often, arrows on strings are used to distinguish LL and RR, and most or all other labels are left implicit; so the zigzag identities, for instance, become:

Minimal string diagram of first zigzag identity (for 'Adjunction')         Minimal string diagram of second zigzag identity (for 'Adjunction')

Properties

Relation to monads

See at monad – Relation between adjunctions and monads.

Examples

Adjoint functors

Proposition

An adjunction in the 2-category Cat of categories, functors and natural transformations is equivalently a pair of adjoint functors.

See also the proof here at adjoint functor.
Proof

Suppose given functors L:CDL \,\colon\, C \to D, R:DCR: D \to C and the structure of a pair of adjoint functors in the form of a natural isomorphism of hom-sets (here)

Ψ c,d:hom D(L(c),d)hom C(c,R(d)) \Psi_{c, d} \;\colon\; \hom_D(L(c), d) \cong \hom_C(c, R(d))

Now the idea is that, in the spirit of the (proof of the) Yoneda lemma, we would like Ψ\Psi to be determined by what it does to identity morphisms. With that in mind, define the adjunction unit η:1 CRL\eta \colon 1_C \to R L by the formula η c=Ψ c,L(c)(1 L(c))\eta_c = \Psi_{c, L(c)}(1_{L(c)}). Dually, define the counit ε:LR1 D\varepsilon \,\colon\, L R \to 1_D by the formula

ε dΨ R(d),d 1(1 R(d)). \varepsilon_d \,\coloneqq\, \Psi^{-1}_{R(d), d}(1_{R(d)}) \,.

Then given g:L(c)dg \,\colon\, L(c) \to d, the claim is that

Ψ c,d(g)=(cη cR(L(c))R(g)R(d)). \Psi_{c, d}(g) \,=\, (c \stackrel{\eta_c}{\to} R(L(c)) \stackrel{R(g)}{\to} R(d)) \,.

This may be left as an exercise in the yoga of the Yoneda lemma, applied to hom D(L(c),)hom C(c,R())\hom_D(L(c), -) \to \hom_C(c, R(-)). By formal duality, given f:cR(d)f \,\colon\, c \to R(d),

Ψ c,d 1(f)=(L(c)L(f)L(R(d))ε dd). \Psi^{-1}_{c, d}(f) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d) \,.

(We spell out the Yoneda-lemma proof of this dual form below.)

Finally, these operations should obviously be mutually inverse, but that can again be entirely encapsulated Yoneda-wise in terms of the effect on identity maps. Thus, if η cΨ c,L(c)(1 L(c))\eta_c \coloneqq \Psi_{c, L(c)}(1_{L(c)}), via the recipe just given for Ψ 1\Psi^{-1} we recover

1 L(c)=(L(c)L(η c)LRL(c)ε L(c)L(c))1_{L(c)} = (L(c) \stackrel{L(\eta_c)}{\to} L R L(c) \stackrel{\varepsilon_{L(c)}}{\to} L(c))

and this is one of the famous triangle identities: 1 L=(LLηLRLεLL)1_L = (L \stackrel{L \eta}{\to} L R L \stackrel{\varepsilon L}{\to} L). Here, juxtaposition of functors and natural transformations denotes neither functor application, nor vertical composition, nor horizontal composition, but whiskering. By duality, we have the other triangle identity 1 R=(RηRRLRRεR)1_R = (R \stackrel{\eta R}{\to} R L R \stackrel{R \varepsilon}{\to} R). These two triangular equations are enough to guarantee that the recipes for Ψ\Psi and Ψ 1\Psi^{-1} indeed yield mutual inverses.

In conclusion it is perfectly sufficient to define an adjoint pair of functors in CatCat as given by unit and counit transformations η:1 CRL\eta: 1_C \to R L, ε:LR1 D\varepsilon: L R \to 1_D, satisfying the triangle identities above.

Remark

The definition of adjunctions via units and counits is an “elementary” definition (so that by implication, the formulation in terms of hom-isomorphismsunctor#InTermsOfHomIsomorphism) is not elementary) in the sense that while the hom-functor formulation relies on some notion of hom-*set*, the formulation in terms of units and counits is purely in the first-order language of categories and makes no reference to a model of set theory. The definition via (co)units therefore gives us a definition of adjunctions even if an assumption of local smallness is not made.

Proof

(Yoneda-lemma argument)
We claim that Ψ c,d 1:hom C(c,R(d))hom D(L(c),d)\Psi^{-1}_{c, d} \,\colon\, \hom_C(c, R(d)) \to \hom_D(L(c), d) can be defined by the formula

Ψ c,d 1(f:cR(d))=(L(c)L(f)L(R(d))ε dd)\Psi^{-1}_{c, d}(f: c \to R(d)) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d)

where ε dΨ R(d),d 1(1 R(d))\varepsilon_d \coloneqq \Psi^{-1}_{R(d), d}(1_{R(d)}). This is by appeal to the proof of the Yoneda lemma applied to the transformation

Ψ ,d 1:hom C(,R(d))hom D(L(),d)\Psi^{-1}_{-, d}: \hom_C(-, R(d)) \to \hom_D(L(-), d)

For the naturality of Ψ 1\Psi^{-1} in the argument ()(-) would imply that given f:cR(d)f: c \to R(d), we have a commutative square

hom C(R(d),R(d)) Ψ R(d),d 1 hom D(L(R(d)),d) hom C(f,R(d)) hom D(L(f),d) hom C(c,R(d)) Ψ c,d 1 hom D(L(c),d)\array{ \hom_C(R(d), R(d)) & \stackrel{\Psi^{-1}_{R(d), d}}{\to} & \hom_D(L(R(d)), d) \\ \hom_C(f, R(d)) \big\downarrow & & \big\downarrow \hom_D(L(f), d) \\ \hom_C(c, R(d)) & \underset{\Psi^{-1}_{c, d}}{\to} & \hom_D(L(c), d) }

Chasing the element 1 R(d)1_{R(d)} down and then across, we get f:cR(d)f: c \to R(d) and then Ψ c,d 1(f)\Psi^{-1}_{c, d}(f). Chasing across and then down, we get ε d\varepsilon_d and then ε dL(f)\varepsilon_d \circ L(f). This completes the verification of the claim.

Corollary

An adjunction in its core 2-groupoid Core(Cat)Core(Cat) is an adjoint equivalence.

Enriched adjoint functors

Similarly one sees:

Example

For VV a cosmos for enrichment, an adjunction in the 2-category VCat of VV-enriched categories is equivalently a pair VV-enriched functors.

Example

Let U:GrpSetU \,\colon\, Grp \to Set from Grp to Set denote the usual forgetful functor from Grp to Set. When we say “F(X)F(X) is the free group generated by a set XX”, we mean there is a function η X:XU(F(X))\eta_X \,\colon\, X \to U(F(X)) which is universal among functions from XX to the underlying set of a group, which means in turn that given a function f:XU(G)f: X \to U(G), there is a unique group homomorphism g:F(X)Gg \colon F(X) \to G such that

f=(Xη XU(F(X))U(g)U(G)) f = (X \stackrel{\eta_X}{\to} U(F(X)) \stackrel{U(g)}{\to} U(G))

Here η X\eta_X is a component of what we call the unit of the adjunction FUF \dashv U, and the equation above is a recipe for the relationship between the map g:F(X)Gg: F(X) \to G and the map f:XU(G)f: X \to U(G) in terms of the unit.

Adjoint (,1)(\infty,1)-functors

(Riehl & Verity 2015, Rem. 4.4.5; Riehl & Verity 2022, Prop. F.5.6; see there for more).

Remark

In view of Prop. , the remarkable aspect of Prop. is that the homotopy 2-category of \infty -categories is sufficient to detect adjointness of \infty -functors, which would, a priori, be defined as a kind of higher homotopy-coherent adjointness in the full ( , 2 ) (\infty,2) -category Cat (,1) Cat_{(\infty,1)} . For more on this reduction of homotopy-coherent adjunctions to plain adjunctions see Riehl & Verity 2016, Thm. 4.3.11, 4.4.11.

References

Adjunctions in 2-categories were introduced (together with the notion of strict 2-categories itself) in:

Though see also the following, which uses more modern terminology:

  • Max Kelly, §2 in: Adjunction for enriched categories, in: Reports of the Midwest Category Seminar III, Lecture Notes in Mathematics 106, Springer (1969) [doi:10.1007/BFb0059145]

A thorough 2-categorical account is contained in:

  • Claude Auderset?, Adjonctions et monades au niveau des 22 -catégories, Cahiers de topologie et géométrie différentielle 15.1 (1974): 3-20.

  • Stephen Schanuel and Ross Street, The free adjunction, Cahiers de topologie et géométrie différentielle catégoriques 27.1 (1986): 81-8

Review:

Fr the special case of adjoint functors see any text on category theory (and see the references at adjoint functor), for instance:

For some early history and illustrative examples see

  • Joachim Lambek, The Influence of Heraclitus on Modern Mathematics, In Scientific Philosophy Today: Essays in Honor of Mario Bunge, edited by Joseph Agassi and Robert S Cohen, 111–21. Boston: D. Reidel Publishing Co. (1982) (doi:10.1007/978-94-009-8462-2_6)

    (more along these lines at objective logic).

The fundamental role of adjoint functors in logic/type theory originates with the observaiton that substitution forms an adjoint triple with existential quantification and universal quantification:

Adjunctions in programming languages (though mainly again just adjoint functors):

  • Ralf Hinze, Generic Programming with Adjunctions, In: J. Gibbons (ed.) Generic and Indexed Programming Lecture Notes in Computer Science, vol 7470. Springer 2012 (pdf, slides doi:10.1007/978-3-642-32202-0_2)

  • Jeremy Gibbons, Fritz Henglein, Ralf Hinze, Nicolas Wu, Relational Algebra by Way of Adjunctions, Proceedings of the ACM on Programming Languages archive Volume 2 Issue ICFP, September 2018 Article No. 86 (pdf, doi:10.1145/3236781)

See also


Last revised on February 14, 2024 at 22:16:57. See the history of this page for a list of all contributions to it.